What is the point of this? Many of our users don't use vscode or docker images, and this forces a particular docker image base in the docker file.

The purpose of this is to provide people a link they can click (https://gitpod.io/#https://github.com/stanford-centaur/PyPantograph) which puts them instantly in an environment with a running jupyter notebook.

This is a draft for now as I didn't get as far as testing it.

The purpose of this is to provide people a link they can click (https://gitpod.io/#https://github.com/stanford-centaur/PyPantograph) which puts them instantly in an environment with a running jupyter notebook.

This is a draft for now as I didn't get as far as testing it.

I think it would be a better idea to have this in a separate repository, where the running environment also provides other Lean interfaces.

I don't use gitpod, vscode, or docker, and this just adds to the maintenance burden for every version update.